We develop a correspondence between the structure of Turing machines and the structure of singularities of real analytic functions, based on connecting the Ehrhard-Regnier derivative from linear logic with the role of geometry in Watanabe's singular learning theory. The correspondence works by embedding ordinary (discrete) Turing machine codes into a family of noisy codes which form a smooth parameter space. On this parameter space we consider a potential function which has Turing machines as critical points. By relating the Taylor series expansion of this potential at such a critical point to combinatorics of error syndromes, we relate the local geometry to internal structure of the Turing machine. The potential in question is the negative log-likelihood for a statistical model, so that the structure of the Turing machine and its associated singularity is further related to Bayesian inference. Two algorithms that produce the same predictive function can nonetheless correspond to singularities with different geometries, which implies that the Bayesian posterior can discriminate between distinct algorithmic implementations, contrary to a purely functional view of inference. In the context of singular learning theory our results point to a more nuanced understanding of Occam's razor and the meaning of simplicity in inductive inference.

Deep Learning experiments have critical requirements regarding the careful handling of their datasets as well as the efficient and correct usage of APIs that interact with hardware accelerators. On the one hand, software mistakes during data handling can contaminate experiments and lead to incorrect results. On the other hand, poorly coded APIs that interact with the hardware can lead to sub-optimal usage and untrustworthy conclusions. In this work we investigate the use of Linear Logic for the analysis of Deep Learning experiments. We show that primitives and operators of Linear Logic can be used to express: (i) an abstract representation of the control flow of an experiment, (ii) a set of available experimental resources, such as API calls to the underlying data-structures and hardware as well as (iii) reasoning rules about the correct consumption of resources during experiments. Our proposed model is not only lightweight but also easy to comprehend having both a symbolic and a visual component. Finally, its artifacts are themselves proofs in Linear Logic that can be readily verified by off-the-shelf reasoners.

Particularly in transgender and nonbinary (TGNB) communities, it is an increasingly common practice to publicly share one's personal pronouns so that we may be gendered correctly in others' speech. Many of us have nuanced desires for how we are gendered, leading us to use more complex descriptions of our wishes; for example, the descriptor 'she/they'. We observe that these descriptions of our wishes have the structure of a little language all their own. We thus propose formal logic as a tool for expressing one's personal pronouns and potentially other aspects of gender. We explore three potential logical foundations (linear logic, temporal logic, and free logic with definite descriptions) and their trade-offs. Our foremost motivation for this proposal is play, affirming that one can be both a logician and TGNB at the same time. We present formalization as something that can continue to evolve over time with society's understanding of gender. This implies that outreach is a major potential application: we can show TGNB youth that they belong in logic and have a unique contribution to make. Tools for evaluating whether one's pronouns are respected are an application as well.

In multiagent systems autonomous agents interact with each other to achieve individual and collective goals. Typical interactions concern negotiation and agreement on resource exchanges. Modeling and formalizing these agreements pose significant challenges, particularly in capturing the dynamic behaviour of agents, while ensuring that resources are correctly handled. Here, we propose exchange environments as a formal setting where agents specify and obey exchange policies, which are declarative statements about what resources they offer and what they require in return. Furthermore, we introduce a decidable extension of the computational fragment of linear logic as a fundamental tool for representing exchange environments and studying their dynamics in terms of provability.

In recent years, many tools have been proposed to design interactive scenarios. The aim of these tools is to provide users with a framework in order to write a story with many branches which will be unfolded by an artificial intelligence application. However, the consistency and quality of the generated narratives are not guaranteed (deadlocks, flaws, etc.). Previous work has defined the properties of a valid interactive scenario and proposed an approach as well as a tool based on a formal model, Linear Logic, to validate these properties. Nevertheless, the application of this tool requires many special skills and so is not really suitable for normal users. In this paper, we present an authoring tool which allows modeling interactive scenarios and analysing them at the structural level using the deduction rules in Linear Logic. Thanks to our tool, normal users are able to create and validate interactive scenarios in comparison with a rich set of predefined properties/criteria of quality.

We present a rule specification language called Ceptre,intended to enable rapid prototyping for experimental game mechanics, especially in domains that depend on procedural generation and multi-agent simulation. Ceptre can be viewed as an explication of a new methodology for understanding games based on linear logic, a formal logic concerned with resource usage. We present a correspondence between gameplay and proof search in linear logic, building on prior work on generating narratives. In Ceptre, we introduce the ability to add interactivity selectively into a generative model, enabling inspection of intermediate states for debugging and exploration as well as a means of play. We claim that this methodology can support game designers and researchers in designing, anaylzing, and debugging the core systems of their work in generative, multi-agent gameplay. To support this claim, we provide two case studies implemented in Ceptre, one from interactive narrative and one from a strategy-like domain.

Linear logic [Gir87] comprises a rich and fascinating formal system that summarizes, in a nuanced way, the way logical inference works if one treats the pool of potential premises of inferences as a resource to be meted out and accounted for. The linear logic abstractions can be applied to practical reasoning systems in a variety of different ways, and can be grounded in concrete domain-specific inference formalisms via multiple routes as well. Here we connect linear logic to uncertain reasoning based on observational semantics. Beginning with a simple semantics for propositions, based on counting observations, we argue that probabilistic and fuzzy logic correspond to two different heuristic assumptions regarding the combination of propositions whose evidence bases are not currently available. These two different heuristic assumptions lead to two different sets of formulas for propagating quantitative truth values through lattice operations. Given this setup, it becomes immediately apparents that these two sets of formulas instantiate the same algebraic and conceptual relationships as the multiplicative and additive operator-sets in linear logic. The standard rules of linear logic then emerge as consequences of the underlying semantics of fuzzy and probabilistic evidence management.

Linear Logic and Defeasible Logic have been adopted to formalise different features of knowledge representation: consumption of resources, and non monotonic reasoning in particular to represent exceptions. Recently, a framework to combine sub-structural features, corresponding to the consumption of resources, with defeasibility aspects to handle potentially conflicting information, has been discussed in literature, by some of the authors. Two applications emerged that are very relevant: energy management and business process management. We illustrate a set of guide lines to determine how to apply linear defeasible logic to those contexts.

-- a group of intelligent agents which fulfill a set of tasks in parallel is represented first by the tensor multiplication of corresponding processes in a linear logic game category. An optimal itinerary in the configuration space of the group states is defined as a play with maximal total reward in the category. New moments also are: the reward is represented as a degree of certainty (visibility) of an agent goal, and the system goals are chosen by the greatest value corresponding to these processes in the system goal lattice. The artificial intelligence is represented in the Artificial General Intelligence (AGI) approach as an information processor which consumes and gives out information. Investigations in the field are focused on systems which act rationally. A formal description of the most intelligent agent (AIXI) behavior, in the sense of some intelligence measure, is suggested in AGI framework [1].

Linear Logic and Defeasible Logic have been adopted to formalise different features relevant to agents: consumption of resources, and reasoning with exceptions. We propose a framework to combine sub-structural features, corresponding to the consumption of resources, with defeasibility aspects, and we discuss the design choices for the framework.